COMMENT ⊗   VALID 00005 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	(wipe-out)
C00003 00003	selection: 7 lines
C00005 00004	diagonalisation: 13 lines			***bug?***
C00010 00005	the proof of ramsey's theorem: 11 lines
C00017 ENDMK
C⊗;
(wipe-out)
(get-proofs natset prf prf jk) ;need the natset file
;time: 34s
;selection: 7 lines
;4s

(PROOF SELECT)

(DEFINE SELECT |∀F A.SELECT(F,A)=(IF UNBOUND(INVERSE(F,A,0)) THEN 0 ELSE 1)|)
(label simpinfo)

(DECL STABILIZE (TYPE: |@FUNCT⊗@SET→@SET|))
(DEFINE STABILIZE
        |∀F A.STABILIZE(F,A)=
	      (IF UNBOUND(INVERSE(F,A,0)) THEN INVERSE(F,A,0) ELSE INVERSE(F,A,1))|)
(label simpinfo) 

(TRW |SELECT(F,A)=0∨SELECT(F,A)=1| (OPEN SELECT))
;SELECT(F,A)=0∨SELECT(F,A)=1
(label simpinfo)

(TRW |STABILIZE(F,A)⊂A| (OPEN STABILIZE))
;STABILIZE(F,A)⊂A
(label simpinfo)

(TRW |NεSTABILIZE(F,A)⊃F(N)=SELECT(F,A)| (OPEN STABILIZE SELECT INVERSE EPSILON))
;NεSTABILIZE(F,A)⊃F(N)=SELECT(F,A)
(label stabselprop)

(TRW |(∀N.F(N)=0∨F(N)=1)∧UNBOUND(A)⊃UNBOUND(STABILIZE(F,A))|
     (OPEN STABILIZE) (USE SPLIT_UNBOUND))
;(∀N.F(N)=0∨F(N)=1)∧UNBOUND(A)⊃UNBOUND(STABILIZE(F,A))
(label splitprop)
;diagonalisation: 13 lines			***bug?***
;11s
(PROOF DIAGONALIZE)

(ASSUME |∀N.SEQ(N')⊂SEQ(N)∧UNBOUND(SEQ(N))|)
(label diagonal_assumption)
 
(UE (REL |λN M.SEQ(M)⊂SEQ(N)|) TRANSITIVE_INDUCTION
    (USE DIAGONAL_ASSUMPTION)
    (PART 1 (OPEN TRANSITIVE INCLUSION)))
;∀N M.N<M⊃SEQ(M)⊂SEQ(N)
;deps: (DIAGONAL_ASSUMPTION)
(label diagonal_step1)
 
(DEFINE DIAGSET |∀N.DIAGSET(N)≡(∀M.MεDIAGSET∩SEGM(N)⊃NεSEQ(M))| 
	(USE COURSE_OF_VALUES_DEFINITION))

;;****PDL-OVERFLOW
;;****QUIT

(TRW |∀N M.N<M∧DIAGSET(N)∧DIAGSET(M)⊃MεSEQ(N)|
     (OPEN EPSILON SEGM INTERSECTION DIAGSET))
;∀N M.N<M∧DIAGSET(N)∧DIAGSET(M)⊃MεSEQ(N)
(label diagonal_step2)

(ASSUME |¬UNBOUND(DIAGSET)|)
(label assume_not)

(RW ASSUME_NOT (USE BOUNDFACT MODE: ALWAYS) (OPEN INCLUSION EPSILON SEGM))
;∀N.DIAGSET(N)⊃N<BOUND(DIAGSET)
;deps: (ASSUME_NOT)
(label diagset_bound)

;find a counter example
(DECL CTR (SORT: NATNUM))
(DEFINE CTR |CTRεSEQ(BOUND(DIAGSET))∧¬(CTRεSEGM(BOUND(DIAGSET)))|
	(DER DIAGONAL_ASSUMPTION INCLUSIONDEF UNBOUNDEF EPSILONDEF))
(label counterexample)

(TRW |∀M.DIAGSET(M)⊃(SEQ(M))(CTR)| 
     (DER DIAGSET_BOUND DIAGONAL_STEP1 INCLUSIONDEF EPSILONDEF COUNTEREXAMPLE))
;∀M.DIAGSET(M)⊃(SEQ(M))(CTR)
;deps: (DIAGONAL_ASSUMPTION ASSUME_NOT)

(TRW |DIAGSET(CTR)| (OPEN DIAGSET EPSILON INTERSECTION) (USE *))
;DIAGSET(CTR)
;deps: (DIAGONAL_ASSUMPTION ASSUME_NOT)
 
(RW COUNTEREXAMPLE (OPEN EPSILON SEGM))
;(SEQ(BOUND(DIAGSET)))(CTR)∧¬CTR<BOUND(DIAGSET)
;deps: (DIAGONAL_ASSUMPTION)

(TCI (ASSUME_NOT) FALSE (DER -1 -2 DIAGSET_BOUND))
;UNBOUND(DIAGSET)
;deps: (DIAGONAL_ASSUMPTION)

(TCI (DIAGONAL_ASSUMPTION) |∃A.UNBOUND(A)∧∀N M.N<M∧A(N)∧A(M)⊃MεSEQ(N)|
     (DER * DIAGONAL_STEP2))
;(∀N.SEQ(N')⊂SEQ(N)∧UNBOUND(SEQ(N)))⊃
;(∃A.UNBOUND(A)∧(∀N M.N<M∧A(N)∧A(M)⊃MεSEQ(N)))
(label diagonalprop)
;the proof of ramsey's theorem: 11 lines
;19s

(PROOF RAMSEY)

(ASSUME |∀N M.HF(N,M)=0∨HF(N,M)=1|)
(label assumption)

;this is the first stabilisation
(DEFINE STAB1 
   |STAB1(0)=STABILIZE(λXV.HF(0,XV),UNIV)∧
    (∀N.STAB1(N')=STABILIZE(λXV.HF(N',XV),STAB1(N)))|
   (USE INDUCTIVE_SET_DEFINITION))
 
;establish two facts for diagonalisation

(TRW |∀N.STAB1(N')⊂STAB1(N)| (OPEN STAB1))
;∀N.STAB1(N')⊂STAB1(N)

(UE (A |λXV.UNBOUND(STAB1(XV))|) PROOF_BY_INDUCTION
    (USE SPLITPROP ASSUMPTION) (OPEN STAB1))
;∀N.UNBOUND(STAB1(N))
;deps: (ASSUMPTION)

;now diagonalize
(DEFINE HOM1 |UNBOUND(HOM1)∧(∀N M.N<M∧HOM1(N)∧HOM1(M)⊃MεSTAB1(N))|
	(USE -1 -2) (USE DIAGONALPROP UE: ((SEQ . STAB1))))
;deps: (ASSUMPTION)
(label hom1prop)

;define the value of h on diagonal sets
(DEFINE STABF |STABF(0)=SELECT(λXV.HF(0,XV),UNIV)∧
	       ∀N.STABF(N')=SELECT(λXV.HF(N',XV),STAB1(N))|
	(USE INDUCTIVE_DEFINITION))

;verify the value
(UE (A  |λN.((∀M.MεSTAB1(N)⊃HF(N,M)=STABF(N))∧(STABF(N)=0∨STABF(N)=1))|)
    PROOF_BY_INDUCTION
    (OPEN STABF STAB1) (USE STABSELPROP UE: ((F.|λXV.HF(N,XV)|)) ))
;∀N.(∀M.MεSTAB1(N)⊃HF(N,M)=STABF(N))∧(STABF(N)=0∨STABF(N)=1)
(label stabfprop)

;define the ultimate stable set
(DECL HOM (TYPE: |@SET|))
(DEFINE HOM |HOM=STABILIZE(STABF,HOM1)|)
      
;verify the properties of the stable set
(TRW |UNBOUND(HOM)∧∀N M.(N<M∧HOM(N)∧HOM(M)⊃HF(N,M)=SELECT(STABF,HOM1))|
     (PART 1 (OPEN HOM) (USE HOM1PROP STABFPROP SPLITPROP))
     (PART 2 (OPEN SELECT HOM HOM1 STABILIZE INVERSE) (USE STABFPROP HOM1PROP)))
;UNBOUND(HOM)∧(∀N M.N<M∧HOM(N)∧HOM(M)⊃HF(N,M)=SELECT(STABF,HOM1))
;deps: (ASSUMPTION)

;now wrap it all up
(TCI (ASSUMPTION) |∃HM V.UNBOUND(HM)∧(∀N M.N<M∧HM(N)∧HM(M)⊃HF(N,M)=V)| (USE *))
;(∀N M.HF(N,M)=0∨HF(N,M)=1)⊃(∃HM V.UNBOUND(HM)∧(∀N M.N<M∧HM(N)∧HM(M)⊃HF(N,M)=V))